ds1, ds2:x:Id fp Type, da1, da2:k:Knd fp Type.
ds2  ds1  da2  da1  (ecl(ds2;da2) r ecl(ds1;da1)) 

latex

Definitions	State(ds), suptype(S; T), S  T, x. t(x), eclbase(k;test), t  T, ecl(ds;da), P  Q, x:A. B(x), x(s), State(ds), , eclcatch(a;l), eclthrow(a;n), a.n, [a]*, eclor(a;b), ecland(a;b), eclseq(a;b)
Lemmas	ma-valtype-subtype, ma-state wf, ma-state-subtype, eclbase wf, fpf wf, id-deq wf, Id wf, Kind-deq wf, Knd wf, fpf-sub wf, ecl wf, eclcatch wf, eclthrow wf, eclact wf, eclrepeat wf, eclor wf, ecland wf, eclseq wf